COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	MATHEMATICAL THEORY OF COMPUTATION AND PROGRAM VERIFICATION
C00012 ENDMK
C⊗;
MATHEMATICAL THEORY OF COMPUTATION AND PROGRAM VERIFICATION


	Computer programs are among the largest man-made objects
(in number of working parts).
Often the largest part of the cost and development time of a program
occurs between the time when the first version is complete and the time
when the remaining errors don't contribute substantially to the cost of
use.  Therefore, a major way of reducing the cost of programming is to
improve the debugging process.

	The first proposal to develop a mathematical formalism for
giving the specifications of computer programs and a technique for
making computer-checkable proofs that programs meet their specifications
was made in [McCarthy 1963].  It has turned out that many mathematical
and practical problems have to be solved in order to make this a reality.
At first progress was slow, because it a long time before computer
scientists of suitable mathematical talent diverted their attention from
the more traditional problems of computability, automata theory and
formal syntax.

	Important early results were obtained by McCarthy (posing the
problem, properties of conditional expressions, the recursion induction
proof technique, and formal interpreter semantics for compilers), Floyd
(the inductive assertion method for proving flow chart programs correct),
Burstall (the structural induction method of proof based on the
structure of the data sets), the IBM Vienna Laboratory (application of
interpreter semantics to PL/I), Manna (reduction of proving termination
and correctness to proving formulas in first order logic), Ashcroft
and Manna (correctness of parallel processes), and Scott and his colleagues
(the lattice-theoretic model of computation).

	Since about 1969, program correctness has been one of the most popular
mathematical areas of computer science, and many approaches have been
made to various aspects of the problem.  Different authors have emphasized
different aspects of the problem, and the different systems have overlapping
capabilities.  It is possible in principle to combine all the capabilities
into one system, but in the current state of rapid change and advance, no-one
is likely to succeed before an advance in some area makes his work obsolete.

	The notions of correctness differ for different categories of
program.  The simplest case is typified by a Fortran program for computing
a numerical function or (say) solving a set of linear equations.  There,
the desired properties of the program can be specified by an input-output
relation.  In our opinion, for this class of program, it should now
be possible to make a programmming language (say a regularization of
Fortran) and a proof technique based on inductive assertions, that would make
program proving a practical tool.  Different
problems are posed by compilers (where what has to be proved is a
correspondence between the calculations performed by the source program
and those performed by the machine language
program that results from the compilation), by programs
that run on parallel processors or deal with asynchronous inputs and
outputs like reservation systems or command-and-control systems and by
operating systems whose correctness conditions include maintaining
security and integrity of files.

	There is an important distinction between programs whose correctness
can be acceptably specified by giving the desired mathematical relations
between their inputs and outputs and programs whose meaningful specification
requires assertions about what the program achieves in the physical world.
Proving the correctness of the first kind of program involves purely mathematical
assumptions about the computations performed by the instructions of the
computer or by the statements of the programming language.  On the other hand,
the correctness of the second kind of program involves also assumptions
about the physical world, the information that comes in on the program's
inputs, and the effects of the program's outputs on the world itself.
An extreme example of this kind of program would be one that operates
an anti-missile system.   There, the correct functioning of the program
depends on whether its assumptions about the behavior of radars and
missiles and anti-missiles correspond to the physical specifications of these
devices, and also on whether the assumptions about ballistics and
aerodynamics are correct.  On a more mundane level, the correctness of
and inventory control system depends on assumptions about the behavior of
objects in storage and the behavior of the people in the system.

	The work on program correctness at the Stanford AI Laboratory
is following several lines.  The largest effort is led by David Luckham
and involves man-machine interaction in the generation of verification
conditions for programs and further man-machine interaction in the use
of his first-order-logic theorem prover to prove the first order sentences
that express the correctness of the program.  This work concentrates at
present on the programming language Pascal which was designed by
Wirth in Zurich to express the ideas of Algol in a more orderly and
sound way.  At present, we do not envisage applying proofs of correctness
to COBOL, JOVIAL, FORTRAN, etc.  Instead, when the correctness proof has
been demonstrated in PASCAL or languages descended from it, then it will
be time to advocate that an integrated system for building programs,
compiling them, and proving them correct be developed that will gradually
replace the older languages.

	Another effort is closely integrated with the artificial intelligence
work in representing information about the world led by McCarthy and
Weyhrauch.  This work, as described elsewhere in this proposal, will
allow proving a program correct in its interaction with the world.  To
do this, it is necessary to develop a language for expressing what is
being assumed about the world, and this is also necessary for making
programs that decide what to do by reasoning about the world.